Inference at * 1 
Iof proof for Lemma list extensionality:



1. T : Type
2. a : T List
3. b : T List
4. ||a|| = ||b||
5. i:. (i < ||a||)  (a[i] = b[i])
  a = b 

latex

 by ((((((((((MoveToConcl 3) 
CollapseTHEN (ListInd 2))) 
CollapseTHEN (RAA (D 0)))) 

CoCollapseTHEN (ListInd (-1)))) 
CollapseTHEN (Reduce 0))) 
CollapseTHEN ((Auto_aux (first_nat 
C1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term))) 

latex

C1: 

C1: 3. u : T
C1: 4. v : T List
C1: 5. b:(T List). (||v|| = ||b||)  (i:. (i < ||v||)  (v[i] = b[i]))  (v = b)
C1: 6. T List
C1: 7. u1 : T
C1: 8. v1 : T List
C1: 9. (||[u / v]|| = ||v1||)
C1: 9.  (i:. (i < ||[u / v]||)  ([u / v][i] = v1[i]))
C1: 9.  ([u / v] = v1)
C1: 10. ||v||+1 = ||v1||+1
C1: 11. i:. (i < (||v||+1))  ([u / v][i] = [u1 / v1][i])
C1:   [u / v] = [u1 / v1]
C.

Definitions	, t  T, Y, P  Q, x:A. B(x), ||as||,
Lemmas	length cons, length wf1, non neg length, length wf2, select wf, nat wf